Nuprl Lemma : fpf-compatible-join-iff 0,22

A:Type, eq:EqDecider(A), B:(AType), fgh:a:A fp B(a).
f || g  (h || f  g  h || f & h || g
latex


Definitionst  T, x:AB(x), EqDecider(T), x(s), xt(x), a:A fp B(a), f || g, Prop, P & Q, f  g, P  Q, P  Q, P  Q, f(x), b, Top, x  dom(f), P  Q, False, A, b, , {T}, SQType(T)
Lemmasfpf-compatible-join, bool cases, eqtt to assert, bool sq, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, not wf, fpf-join-ap, fpf-join-dom, assert wf, fpf-dom wf, fpf-trivial-subtype-top, fpf-join wf, fpf-compatible wf, fpf wf, deq wf

origin